Inspecting the properties of logic circuits is pivotal to logic applications for computers and especially to Electronic Design Automation (EDA) [1]. There exists a large variety of properties to be checked in logic circuits, e.g., unateness, linearity, symmetry, balancedness, monotonicity, thresholdness and many others [2]. Basic characteristics are usually verified first to provide grounds for more involved tests. Tautology and contradiction are the most fundamental properties in logic circuits. A check for tautology determines if a logic circuit is true for all possible input patterns. Analogously, a check for contradiction determines if a logic circuit is false for all possible input patterns. While investigating elementary properties, tautology and contradiction check are difficult problems, i.e., co-NP-complete and NP-complete, respectively [3]. Indeed, both tautology and contradiction check are equivalent formulation of the Boolean SATisfiability (SAT) problem [3]. In this scenario, new efficient algorithms for tautology/contradiction check are key to push further the edge of computational limits, enabling larger logic circuits to be examined.
Tautology and contradiction check are dual problems. One can interchangeably check for tautology in place of contradiction by inverting all outputs in a logic circuit. In this trivial approach, the two obtained problems are fully complementary and there is no explicit computational advantage in solving one problem instead of the other.
In the present description, we show that exact logic inversion is not necessary for transforming tautology into contradiction, and vice versa. We give a set of operator switching rules that selectively exchange tautologies with contradictions. A logic circuit modified by our rules is inverted just if identically true or false for all input combinations. In the other cases, it is not necessarily the complement of the original one. In a simple logic circuit made of AND, OR and INV logic operators, our switching rules swap AND/OR operator types. We give a set of rules for general logic circuits in the rest of this paper. Note that in this paper we mostly deal with single output circuits. For multi-output circuits, the same approach can be extended by ORing (contradiction) or ANDing (tautology) the outputs that need to be checked into a single one.
Parallel checking techniques are known from prior art. For example, one can launch in parallel many randomized check runs on the same problem instance with the aim to hit the instance-intrinsic minimum runtime [4]